-----------------------------------------------------------------------------
--
-- Module      :  Types
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  Eduard Sergeev
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level types and operations
--
-----------------------------------------------------------------------------

{-# LANGUAGE MultiParamTypeClasses, TypeOperators, TypeFamilies,
FlexibleInstances, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances #-}


module Data.Unit.Types (

HTrue,
HFalse,
And,
Or,
Not,


Zero,
Succ,
One,
Two,
Three,
Four,

ToPeano,

ToList,
FromList,

Convert,
Unconvert,

Less,
Greater,
LessOrEqual,
GreaterOrEqual,

U,

(:*:),
(:/:),

Singleton,
InsertBefore,

Remove,
Union,
Except,

Mult,
Div,

Plus,
Minus,
Multiply,
Divide,

MApplicative(..),
mlift2M,
--
MApplicative2(..),
mlift2M2,
--

) where

import Data.Function (on)
import Data.Maybe (fromMaybe)
import Data.List (unionBy, intersperse)

import Data.Unit.Type.Internal -- (HTrue, HFalse)


class And a b r
instance (HTrue ~ r) => And HTrue HTrue r
instance (HFalse ~ r) => And HTrue HFalse r
instance (HFalse ~ r) => And HFalse HTrue r
instance (HFalse ~ r) => And HFalse HFalse r


class Or a b r
instance (HFalse ~ r) => Or HFalse HFalse r
instance (HTrue ~ r) => Or HTrue HFalse r
instance (HTrue ~ r) => Or HFalse HTrue r
instance (HTrue ~ r) => Or HTrue HTrue r

class Not a r
instance (HFalse ~ r) => Not HTrue r
instance (HTrue ~ r) => Not HFalse r


---------------------------
-- Peano numbers
---------------------------

-- Numbers
data Zero
data Succ a
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

type family Equal a b :: *
type instance Equal Zero Zero = HTrue
type instance Equal (Succ l) Zero = HFalse
type instance Equal Zero (Succ r) = HFalse
type instance Equal (Succ l) (Succ r) = Equal l r

class Less a b r
instance (HFalse ~ r) => Less Zero Zero r
instance (HTrue ~ r) => Less Zero (Succ a) r
instance (HFalse ~ r) => Less (Succ a) Zero r
instance (Less a b r) => Less (Succ a) (Succ b) r

class Greater a b r
instance (HFalse ~ r) => Greater Zero Zero r
instance (HTrue ~ r) => Greater (Succ a) Zero r
instance (HFalse ~ r) => Greater Zero (Succ a) r
instance (Greater a b r) => Greater (Succ a) (Succ b) r

class LessOrEqual a b r
instance (Greater a b r1, Not r1 r) => LessOrEqual a b r

class GreaterOrEqual a b r
instance (Less a b r1, Not r1 r) => GreaterOrEqual a b r


-- | Conversion
type family ToPeano u :: *
type instance ToPeano U = Zero

{-
type family ToList u :: *
type instance ToList (a :/: b) = (ToList a)  :/: (ToList b)
type instance ToList (a :*: b) = (ToList a)  :*: b
type instance ToList U = U
-}


class ToList u l
instance (ToList a la, ToList b lb, Div la lb r) => ToList (a :/: b) r
instance (ToList a la, ToList b lb, Mult la lb r) => ToList (a :*: b) r
instance (r ~ U) => ToList U r


type family FromList u :: *
type instance FromList (a :/: b) = (FromList a)  :/: (FromList b)
type instance FromList U = U

--class FromList l u
--instance (FromList a la, FromList b lb, r ~ (la :/: lb)) => FromList (a :/: b) r
--instance (r ~ U) => FromList U r


class Convert u c
instance (ToList u c) => Convert u c

--type family Convert u :: *
--type instance Convert u = ToList u

--type family Unconvert u :: *
--type instance Unconvert u = FromList u


class Unconvert c u
instance (FromList c ~ u) => Unconvert c u



-------------------
-- operators
-------------------

data a :*: b
data a :/: b

infixl 7 :*:
infixl 6 :/: 

-- Unit type (1, mzero)
data U
instance Show U where show _ = "1"


--------------------
-- Type List
--------------------

type Singleton a = U :*: a


-- | Inserts an element into the list in accordance to it's 'peano rank'
class InsertBefore c e r
instance (LessOrEqual (ToPeano h) (ToPeano e) p, InsertBefore' p (t :*: h) e r) =>
    InsertBefore (t :*: h) e r
instance ((U :*: e) ~ r) => InsertBefore U e r

class InsertBefore' p c e r
instance ((l :*: e) ~ r) => InsertBefore' HTrue l e r
instance (InsertBefore t e r1, (r1 :*: h) ~ r) => InsertBefore' HFalse (t :*: h) e r


-- | Union for lists
class Union l r u
instance (InsertBefore l h r1, Union r1 t r) => Union l (o t h) r
instance (l ~ r) => Union l U r


-- | Type-level Maybe's Just
data Just a
-- | Type-level Maybe's Nothing
data Nothing

class Remove c e r
instance (AreEqual h e p, Remove' p (t :*: h) e r) => Remove (t :*: h) e r
--instance (Remove' (Equal (ToPeano h) (ToPeano e)) (t :*: h) e r) => Remove (t :*: h) e r
instance ((U,Just e) ~ r) => Remove U e r

class Remove' p c e r
instance ((t,Nothing) ~ r) => Remove' HTrue (t :*: h) e r
instance (Remove t e (t',e'), (t' :*: h) ~ r', (r',e') ~ r) => Remove' HFalse (t :*: h) e r


---
class Except l r e
instance (Remove l h (l1,h1), Except l1 t (l2,e2), IB e2 h1 e3, (l2,e3) ~ le) => Except l (t :*: h) le
instance ((l,U) ~ r) => Except l U r

class IB a b r
instance (InsertBefore l h r) => IB l (Just h) r
instance (r ~ l) => IB l Nothing r


-----------------------
-- Num type operations
-----------------------
class Mult a b r
instance (Mult nl nr rn, Mult dl dr rd, Div rn rd r) => Mult (nl :/: dl) (nr :/: dr) r
instance (Mult (t :*: h) nr rn, Div rn dr r) => Mult (t :*: h) (nr :/: dr) r
instance (Mult (t :*: h) (nl :/: dl) ra) => Mult (nl :/: dl) (t :*: h) ra
instance (Union (tl :*: hl) (tr :*: hr) r) => Mult (tl :*: hl) (tr :*: hr) r
instance ((n :/: d) ~ r) => Mult U (n :/: d) r
instance ((n :*: d) ~ r) => Mult U (n :*: d) r
instance (e ~ r) => Mult e U r


---
class Div n d r
instance (Mult nl dr n, Mult dl nr d, Div n d r) => Div (nl :/: dl) (nr :/: dr) r
instance (Mult dl (tr :*: hr) d, Div nl d r) => Div (nl :/: dl) (tr :*: hr) r
instance (Mult (tl :*: hl) dr n, Div n nr r) => Div (tl :*: hl) (nr :/: dr) r
instance (Except (tl :*: hl) (tr :*: hr) (n',d'), Comb n' d' r) => Div (tl :*: hl) (tr :*: hr) r
instance ((d :/: n) ~ r) => Div U (n :/: d) r
instance ((U :/: n :*: d) ~ r) => Div U (n :*: d) r
instance (e ~ r) => Div e U r


class Comb n d r
instance (U ~ r) => Comb U U r
instance ((U :/: t :*: h) ~ r) => Comb U (t :*: h) r
instance ((t :*: h) ~ r) => Comb (t :*: h) U r
instance ((tl :*: hl :/: tr :*: hr) ~ r) => Comb (tl :*: hl) (tr :*: hr) r


class Plus a b r
instance (a ~ b, a ~ r) => Plus a b r

class Minus a b r
instance (a ~ b, a ~ r) => Minus a b r

class Divide n d r
instance (Convert n cn, Convert d cd, Div cn cd crr, Unconvert crr r) => Divide n d r
--instance (Convert n ~ cn, Convert d ~ cd, Div cn cd crr, Unconvert crr r) => Divide n d r
--instance (Div (Convert2 n) (Convert2 d) rc, Unconvert2 rc ~ r) => Divide n d r
--type family Divide n d :: *
--type instance Divide n d = Div (Convert n) (Convert d) cd, Div cn cd crr, Unconvert crr r) => Divide n d = r

class Multiply a b r

--instance (Mult (Convert n) (Convert d) rc, Unconvert rc ~ r) => Multiply n d r
instance (Convert a ca, Convert b cb, Mult ca cb cr, Unconvert cr r) => Multiply a b r


--type family a :**: b :: *  

class Aa a b where
    type Bb a b :: * -> *
--type instance a :**: b = (Multiply a b r) => r


---------------------
-- Show and related
---------------------
class Repr a where
    repr :: a -> [String]

instance Repr U where
    repr _ = ["1"]

instance (Repr t , Show h) => Repr (t :*: h) where
    repr _ = repr (undefined :: t) ++ [show (undefined :: h)]

--instance (Repr (a :*: b)) => Show (a :*: b)  where
instance (ToList (a :*: b) r, Repr r) => Show (a :*: b) where
    show _ = comb . repr $ (undefined :: r)
        where
          comb = concat . intersperse "*" . snd . foldr it (("",0),[])
              where
                it e ((l,n),rs) | e == l = ((l,n+1),rs)
                it e ((_,0),rs) = ((e,1),rs)
                it e ((l,1),rs) = ((e,1), l : rs)
                it e ((l,n),rs) = ((e,1), (l ++ "^" ++ show n) : rs)

instance (Show a, Show b) => Show (a :/: b) where
    show _ = show (undefined::a) ++ "/" ++ show (undefined::b)


-- | Some variation on the theme of Applicative
class MApplicative a where
    mpure :: c -> a b c
    (<***>) :: a b (c -> d) -> a e c -> a g d

mlift2M :: (MApplicative a) => (x -> y -> z) -> a b x -> a c y -> a d z
mlift2M f l r = mpure f <***> l <***> r

class MApplicative2 a where
    mpure2 :: n -> a n c
    (<****>) :: a (c -> d) b -> a c e -> a d g

mlift2M2 :: (MApplicative2 a) => (x -> y -> z) -> a x b -> a y c -> a z d
mlift2M2 f l r = mpure2 f <****> l <****> r




